$\forall$$R$:Realizer, $i$:Id. R{-}Feasible($R$) $\Rightarrow$ R{-}da($R$;$i$) $=$ 1of(2of([[$R$]]($i$))) $\in$ $k$:Knd fp$\rightarrow$ Type